\begin{tabbing}
$k$(v:$B$) sends on $l$ [${\it tg}$:$T$, $f$ $<$state, v$>$]?[]
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(($\forall$$x$:Id. vartype(source($l$);$x$) $\subseteq$r ${\it ds}$($x$)?Top)\+
\\[0ex]\& ($\forall$$e$:E. (loc($e$) = source($l$)) $\Rightarrow$ (kind($e$) = $k$) $\Rightarrow$ (valtype($e$) $\subseteq$r $B$))
\\[0ex]\& ($\forall$$e$:E. (kind($e$) = rcv($l$,${\it tg}$)) $\Rightarrow$ (valtype($e$) $\subseteq$r $T$)))
\\[0ex]c$\wedge$ \=($\forall$$e$:E.\+
\\[0ex](loc($e$) = source($l$))
\\[0ex]$\Rightarrow$ (kind($e$) = $k$)
\\[0ex]$\Rightarrow$ \=((\=($\uparrow$can{-}apply($f$;$<$(state when $e$), val($e$)$>$))\+\+
\\[0ex]$\Rightarrow$ ($\exists$\=${\it e'}$:E\+
\\[0ex]((kind(${\it e'}$) = rcv($l$,${\it tg}$))
\\[0ex]c$\wedge$ \=(sender(${\it e'}$) = $e$\+
\\[0ex]\& (\=$\forall$${\it e''}$:E.\+
\\[0ex](kind(${\it e''}$) = rcv($l$,${\it tg}$)) $\Rightarrow$ (sender(${\it e''}$) = $e$) $\Rightarrow$ (${\it e''}$ = ${\it e'}$))
\-\\[0ex]\& val(${\it e'}$) = do{-}apply($f$;$<$(state when $e$), val($e$)$>$)))))
\-\-\-\\[0ex]\& (\=($\neg$($\uparrow$can{-}apply($f$;$<$(state when $e$), val($e$)$>$)))\+
\\[0ex]$\Rightarrow$ ($\neg$($\exists$${\it e'}$:E. ((kind(${\it e'}$) = rcv($l$,${\it tg}$)) c$\wedge$ (sender(${\it e'}$) = $e$)))))))
\-\-\-\-
\end{tabbing}